l:IdLnk, da:k:Knd fp Type, tg:Id. tg  dom(dt(l;da))  rcv(l,tg)  dom(da) 

latex

Definitions

IdLnk, t  T, Knd, x. t(x), x:A. B(x), a:A fp B(a), Id, Top, fpf-domain(f), rcv(l,tg), (x  l), b, A & B, P & Q, x:A. B(x), if b t else f fi, outl(x), isl(x), , Prop, P  Q, P  Q, P  Q, , Unit, tag(k), lnk(k), a = b, isrcv(k), compose-fpf(a;b;f), dt(l;da), KindDeq, IdDeq, x  dom(f), False, True, false, A, b, {T}, SQType(T), P  Q, T

Lemmas

squash wf, bool cases, bool sq, bfalse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-lnk, bool wf, bnot wf, not wf, true wf, false wf, member-fpf-domain, fpf-dom wf, es-dt wf, id-deq wf, Kind-deq wf, iff functionality wrt iff, compose-fpf-dom, isrcv wf, ifthenelse wf, eq lnk wf, lnk wf, tagof wf, unit wf, it wf, assert wf, l member wf, rcv wf, fpf-domain wf, fpf-trivial-subtype-top, Id wf, fpf wf, Knd wf, IdLnk wf